$\forall$${\it es}$:event\_system\{i:l\}, $i$:Id, ${\it ds}$:fpf(Id; $x$.Type).
\\[0ex]($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}state(${\it es}$; $i$); decl{-}state(${\it ds}$))